$\forall$$A$:Type, $f$:($A$$\rightarrow\mathbb{B}$), $L$:$A$ List. \\[0ex](1of(split\_tail($L$ $\mid$ $\forall$$x$.$f$($x$))) @ 2of(split\_tail($L$ $\mid$ $\forall$$x$.$f$($x$)))) $=$ $L$